計算木論理 (CTL)
computational tree logic
演算子
經路限定子 (path quantifier)
all :$ Ap分岐する全ての經路で眞。經路に關する全稱
exists :$ Ep眞である經路が分岐の中に存在する。經路に關する特稱
時相演算子 (temporal operator)
next :$ Xp次の時點で眞
globally :$ Gp今後常に眞。時點に關する全稱
finally :$ Fp孰れ眞に成る。時點に關する特稱
until :$ pUq孰れ$ qが眞に成り、$ qが眞に成る直前迄は$ pが眞
weak until (unless) :$ pWq$ qが眞に成る直前迄は$ pが眞
經路限定子と時相演算子が續いた演算子 ($ AXp、$ A(pUq)等) のみが有效
最小の例は$ \lbrace\bot,\lor,\neg,EG,EU,EX\rbrace
線形時相論理 (LTL) と比べ、分岐を表現できる($ AG(p\to EFq)等)が、時相演算子を二つ續けて竝べられない($ GFp等) CTL*
fair CTL
probabilistic CTL